(in-package "ACL2")
(include-book "avl-integer-keys")

;;;Implementation of IXMLParser.
;;;Note: unless stated otherwise,
;;;"string" variables are actually
;;;lists of characters.
;;;
;;;A common pattern in these functions
;;;is returning a list of two elements,
;;;where the first is the result value of 
;;; whatever was parsed, and the second is a list of 
;;; the characters still waiting to be parsed.
(include-book "list-utilities")

;;Predicate that returns true if 
;;str begins with prefix.
(defun begins-with (str prefix)
  (if (consp prefix)
      (if (equal (car str) (car prefix))
          (begins-with (cdr str)
                       (cdr prefix))
          nil)
      t))

;;Split str into two lists of characters:
;;first: all characters before first instance of chr,
;;second: all characters after first instance of chr.
(defun break-at-and-drop (chr str)
  (let* ((b-a (break-at chr str)))
    (list (car b-a) (cdadr b-a))))

;;helper for removing whitespace from a list of characters.
;;moves string to accumulation parameter with whitespace removed.
;;This reverses the list.
(defun strip-ws-h (str acc)
  (if str
      (if (or 
              (equal (car str) #\newline)
              (equal (car str) #\tab)
              (equal (car str) #\space))
          (strip-ws-h (cdr str) acc)
          (strip-ws-h (cdr str) (cons (car str) acc)))
      acc))

;;strip all whitespace from a list of characters.
;;returns the same string with whitespace remove.d
(defun strip-ws (str)
  (reverse (strip-ws-h str nil)))

;;Read an XML literal from the front of 
;;a list of chars.
;;Return type: the literal at the front
;; of the list of characters,
;; followed by all the characters afterward.
(defun read-literal (str)
  (break-at #\< str))

;;Parse a tag from the beginning of a list
;;of characters.
;;Return: the name of a tag, followed by
;;all the text after the tag.
(defun parse-tag (chrs)
  (break-at-and-drop #\> (cdr chrs)))

;;Remove an end tag from the front of a list
;;of characters.
;;Return: All the text after the first end
;; tag.
(defun parse-end-tag (chrs)
  (cadr (break-at-and-drop #\> chrs)))

;;wrapper so that XML children can appear
;;inside XML bodies, by allowing parse-body to
;;call parse-xml, even though parse-xml calls it.
(mutual-recursion
 
 ;;helper for parsing an XML body element from the front
 ;;of a list of charcters, generating
 ;;an association list of charcters in res.
 (defun parse-body-h (chrs res)
   (declare (xargs :measure chrs))
   (if (consp chrs)
       (cond ((begins-with chrs (str->chrs "</"))
              (list res chrs))
             ((begins-with chrs (str->chrs "<"))
              (let* ( (rec-xml (parse-xml chrs))
                      (rec-xml-contents (car rec-xml))
                      (chr2 (cadr rec-xml)))
                (parse-body-h chr2 (cons rec-xml-contents res))))
             (t (let* ((lit (read-literal chrs))
                       (lit-con (car lit))
                       (chr2 (cadr lit)))
                  (list (chrs->str lit-con) chr2))))
       (list res chrs)))
 
 ;;Function to parse an XML element from the front of
 ;;a list of characters. 
 ;;Return type: The results of the parsing, followed by
 ;; the remainder of the string after parsing the first
 ;; full XML element.
 (defun parse-xml (chrs)
   (declare (xargs :measure chrs))
   (let* ((pt-result (parse-tag chrs))
          (tag (car pt-result))
          (chr2 (cadr pt-result))
          (pb-result (parse-body chr2))
          (body (car pb-result))
          (chr3 (cadr pb-result)))
     (list (list (chrs->str tag) body) (parse-end-tag chr3))))
 
 ;;Function to parse an XML body element from the front of a
 ;;list of characters.
 ;;Return types: A list of
 ;; 1. the parse results as -
 ;;    strings for simple bodies, association lists as returned
 ;;    by parse-xml for nontrivial bodies.
 ;; 2. The remainder of the string after parsing the first
 ;;  body element.
 (defun parse-body (chrs)
   (declare (xargs :measure chrs))
   (let* ((results (parse-body-h chrs nil))
          (body (car results))
          (rem (cdr results)))
     (if body ;return "" instead of nil if body is empty.
         results
         (cons "" rem))))
 );;end mutual recursion tag

;;Helper function for parsing a set of XML elements from a 
;;list of characters after whitespace has been stripped.
(defun parse-xml-doc-h (str)
  (if (endp str)
      nil
      (let* ((after-round (parse-xml str))
             (xml-elem (car after-round))
             (rest (cadr after-round)))
        (cons xml-elem (parse-xml-doc-h rest)))))

;;Function for parsing a list of XML elements, as described in
;;the interface. Note: str is a LIST OF CHARACTERS
(defun parse-xml-doc (str)
  (parse-xml-doc-h (strip-ws str)))

  (defconst *a-lifelike-xml* "<ruleType>lifelike</ruleType>
  <birthStates><state>4</state><state>3</state></birthStates>
  <deathStates><state>2</state><state>6</state></deathStates>")
  
  (defconst *an-elementary-xml* "<ruleType>elemenetary</ruleType><wolframCode>254</wolframCode>")